T:(i:Id{k:Knd| hasloc(k;i)} Type), P:(i:Idk:{k:Knd| hasloc(k;i)} T(i,k)), ik:LocKnd.
let i,k:LocKnd = ik in P(i,k)  T(ik.1,ik.2) 

latex

Definitions	Type, t  T, x:A. B(x), hasloc(k;i), b, Knd, {x:A| B(x)} , x:AB(x), Id, f(a), x(s1,s2), let x,y = A in B(x;y), x:A  B(x), let i,k:LocKnd = ik in P(i;k), LocKnd, P  Q, P  Q, <a, b>, P & Q, P  Q, {T}, SQType(T), s = t, , s ~ t, left + right, Atom$n, x.A(x), x. t(x), t.2, t.1
Lemmas	pi1 wf, pi2 wf, Id sq, Knd sq, Id wf, Knd wf, assert wf, hasloc wf